(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Real)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Real)
(declare-fun x_41 () Real)
(declare-fun x_42 () Real)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Real)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(declare-fun x_61 () Real)
(declare-fun x_62 () Real)
(declare-fun x_63 () Real)
(declare-fun x_64 () Real)
(declare-fun x_65 () Real)
(declare-fun x_66 () Real)
(declare-fun x_67 () Real)
(declare-fun x_68 () Real)
(declare-fun x_69 () Real)
(declare-fun x_70 () Real)
(declare-fun x_71 () Real)
(declare-fun x_72 () Real)
(declare-fun x_73 () Real)
(declare-fun x_74 () Real)
(declare-fun x_75 () Real)
(declare-fun x_76 () Real)
(declare-fun x_77 () Real)
(declare-fun x_78 () Real)
(declare-fun x_79 () Real)
(declare-fun x_80 () Real)
(declare-fun x_81 () Real)
(declare-fun x_82 () Real)
(declare-fun x_83 () Real)
(declare-fun x_84 () Real)
(declare-fun x_85 () Real)
(declare-fun x_86 () Real)
(declare-fun x_87 () Real)
(declare-fun x_88 () Real)
(declare-fun x_89 () Real)
(declare-fun x_90 () Real)
(declare-fun x_91 () Real)
(declare-fun x_92 () Real)
(declare-fun x_93 () Real)
(declare-fun x_94 () Real)
(declare-fun x_95 () Real)
(declare-fun x_96 () Real)
(declare-fun x_97 () Real)
(declare-fun x_98 () Real)
(declare-fun x_99 () Real)
(declare-fun x_100 () Real)
(declare-fun x_101 () Real)
(declare-fun x_102 () Real)
(declare-fun x_103 () Real)
(declare-fun x_104 () Real)
(declare-fun x_105 () Real)
(declare-fun x_106 () Real)
(declare-fun x_107 () Real)
(declare-fun x_108 () Real)
(declare-fun x_109 () Real)
(declare-fun x_110 () Real)
(declare-fun x_111 () Real)
(declare-fun x_112 () Real)
(declare-fun x_113 () Real)
(declare-fun x_114 () Real)
(declare-fun x_115 () Real)
(declare-fun x_116 () Real)
(declare-fun x_117 () Real)
(declare-fun x_118 () Real)
(declare-fun x_119 () Real)
(declare-fun x_120 () Real)
(declare-fun x_121 () Real)
(declare-fun x_122 () Real)
(declare-fun x_123 () Real)
(declare-fun x_124 () Real)
(declare-fun x_125 () Real)
(declare-fun x_126 () Real)
(declare-fun x_127 () Real)
(declare-fun x_128 () Real)
(assert (let ((?v_48 (= x_51 x_7)) (?v_61 (= x_53 x_1)) (?v_13 (= x_55 x_2)) (?v_20 (= x_56 x_3)) (?v_27 (= x_57 x_4)) (?v_34 (= x_58 x_5)) (?v_41 (= x_59 x_6)) (?v_106 (= x_10 x_17))) (let ((?v_99 (not ?v_106)) (?v_98 (+ (+ x_17 x_8) x_9))) (let ((?v_142 (= x_10 ?v_98)) (?v_109 (= x_11 x_17))) (let ((?v_100 (not ?v_109)) (?v_146 (= x_11 ?v_98)) (?v_112 (= x_12 x_17))) (let ((?v_101 (not ?v_112)) (?v_150 (= x_12 ?v_98)) (?v_115 (= x_13 x_17))) (let ((?v_102 (not ?v_115)) (?v_154 (= x_13 ?v_98)) (?v_118 (= x_14 x_17))) (let ((?v_103 (not ?v_118)) (?v_158 (= x_14 ?v_98)) (?v_121 (= x_15 x_17))) (let ((?v_104 (not ?v_121)) (?v_162 (= x_15 ?v_98)) (?v_124 (= x_16 x_17))) (let ((?v_105 (not ?v_124)) (?v_166 (= x_16 ?v_98)) (?v_141 (not (<= x_54 x_17))) (?v_145 (not (<= x_46 x_17))) (?v_149 (not (<= x_47 x_17))) (?v_153 (not (<= x_48 x_17))) (?v_157 (not (<= x_49 x_17))) (?v_161 (not (<= x_50 x_17))) (?v_165 (not (<= x_52 x_17)))) (let ((?v_169 (or ?v_141 ?v_142)) (?v_172 (or ?v_145 ?v_146)) (?v_175 (or ?v_149 ?v_150)) (?v_178 (or ?v_153 ?v_154)) (?v_181 (or ?v_157 ?v_158)) (?v_184 (or ?v_161 ?v_162)) (?v_187 (or ?v_165 ?v_166)) (?v_5 (= x_39 0)) (?v_14 (= x_40 0)) (?v_21 (= x_41 0)) (?v_28 (= x_42 0)) (?v_35 (= x_43 0)) (?v_42 (= x_44 0)) (?v_49 (= x_45 0)) (?v_4 (= x_10 x_8)) (?v_15 (= x_11 x_8)) (?v_22 (= x_12 x_8)) (?v_29 (= x_13 x_8)) (?v_36 (= x_14 x_8)) (?v_43 (= x_15 x_8)) (?v_50 (= x_16 x_8)) (?v_62 (= x_54 1)) (?v_16 (= x_46 1)) (?v_23 (= x_47 1)) (?v_30 (= x_48 1)) (?v_37 (= x_49 1)) (?v_44 (= x_50 1)) (?v_51 (= x_52 1)) (?v_10 (= x_21 0)) (?v_17 (= x_24 0)) (?v_24 (= x_27 0)) (?v_31 (= x_30 0)) (?v_38 (= x_33 0)) (?v_45 (= x_36 0)) (?v_52 (= x_20 0)) (?v_9 (= x_22 0)) (?v_18 (= x_25 0)) (?v_25 (= x_28 0)) (?v_32 (= x_31 0)) (?v_39 (= x_34 0)) (?v_46 (= x_37 0)) (?v_53 (= x_19 0)) (?v_11 (= x_23 0)) (?v_19 (= x_26 0)) (?v_26 (= x_29 0)) (?v_33 (= x_32 0)) (?v_40 (= x_35 0)) (?v_47 (= x_38 0)) (?v_54 (= x_18 0)) (?v_6 (= 1 x_8)) (?v_3 (+ 1 1))) (let ((?v_8 (= x_54 ?v_3)) (?v_7 (= (+ x_8 x_9) 1))) (let ((?v_12 (and (not ?v_6) (not ?v_7))) (?v_60 (= x_46 ?v_3)) (?v_64 (= x_47 ?v_3)) (?v_66 (= x_48 ?v_3)) (?v_68 (= x_49 ?v_3)) (?v_70 (= x_50 ?v_3)) (?v_72 (= x_52 ?v_3)) (?v_87 (+ x_0 x_8))) (let ((?v_88 (<= x_10 ?v_87)) (?v_89 (<= x_11 ?v_87)) (?v_90 (<= x_12 ?v_87)) (?v_91 (<= x_13 ?v_87)) (?v_92 (<= x_14 ?v_87)) (?v_93 (<= x_15 ?v_87)) (?v_94 (<= x_16 ?v_87)) (?v_199 (not (<= (- ?v_87 x_127) 1))) (?v_200 (not (>= (- ?v_87 x_128) 1))) (?v_206 (- 1 1))) (let ((?v_201 (not (<= ?v_206 x_126))) (?v_205 (= x_8 ?v_87))) (let ((?v_204 (not ?v_205)) (?v_202 (+ (+ ?v_87 x_8) x_9))) (let ((?v_229 (= x_8 ?v_202))) (let ((?v_203 (and (or ?v_204 (not (>= (+ ?v_87 x_9) 1))) (not ?v_229))) (?v_228 (not (>= ?v_87 1)))) (let ((?v_218 (and ?v_205 ?v_228)) (?v_219 (< x_0 0)) (?v_233 (or ?v_228 ?v_229)) (?v_234 (- 0 x_1))) (let ((?v_230 (* ?v_234 1000)) (?v_243 (- 0 x_7))) (let ((?v_231 (* ?v_243 1000)) (?v_244 (+ 0 x_9))) (let ((?v_245 (and ?v_229 (not (= ?v_244 0)))) (?v_246 (- 0 0)) (?v_2 (* x_39 2)) (?v_55 (- ?v_3 1)) (?v_57 (+ ?v_3 1)) (?v_58 (+ ?v_244 1)) (?v_59 (+ (+ x_8 x_8) x_9)) (?v_56 (* x_40 2)) (?v_63 (* x_41 2)) (?v_65 (* x_42 2)) (?v_67 (* x_43 2)) (?v_69 (* x_44 2)) (?v_71 (* x_45 2)) (?v_73 (- x_54 x_60)) (?v_74 (- x_46 x_60)) (?v_75 (- x_47 x_60)) (?v_76 (- x_48 x_60)) (?v_77 (- x_49 x_60)) (?v_78 (- x_50 x_60)) (?v_79 (- x_52 x_60)) (?v_80 (+ x_54 x_60)) (?v_81 (+ x_46 x_60)) (?v_82 (+ x_47 x_60)) (?v_83 (+ x_48 x_60)) (?v_84 (+ x_49 x_60)) (?v_85 (+ x_50 x_60)) (?v_86 (+ x_52 x_60)) (?v_95 (- x_17 x_127)) (?v_96 (- x_17 x_128)) (?v_97 (+ x_17 x_9)) (?v_107 (- x_53 x_119)) (?v_108 (- x_54 x_112)) (?v_110 (- x_55 x_120)) (?v_111 (- x_46 x_113)) (?v_113 (- x_56 x_121)) (?v_114 (- x_47 x_114)) (?v_116 (- x_57 x_122)) (?v_117 (- x_48 x_115)) (?v_119 (- x_58 x_123)) (?v_120 (- x_49 x_116)) (?v_122 (- x_59 x_124)) (?v_123 (- x_50 x_117)) (?v_125 (- x_51 x_125)) (?v_126 (- x_52 x_118)) (?v_127 (- x_53 x_23)) (?v_128 (- x_54 x_17)) (?v_129 (- x_55 x_26)) (?v_130 (- x_46 x_17)) (?v_131 (- x_56 x_29)) (?v_132 (- x_47 x_17)) (?v_133 (- x_57 x_32)) (?v_134 (- x_48 x_17)) (?v_135 (- x_58 x_35)) (?v_136 (- x_49 x_17)) (?v_137 (- x_59 x_38)) (?v_138 (- x_50 x_17)) (?v_139 (- x_51 x_18)) (?v_140 (- x_52 x_17)) (?v_170 (- x_23 x_119))) (let ((?v_143 (* ?v_170 1000)) (?v_144 (* (- x_23 x_125) 1000)) (?v_147 (* (- x_26 x_119) 1000)) (?v_148 (* (- x_26 x_125) 1000)) (?v_151 (* (- x_29 x_119) 1000)) (?v_152 (* (- x_29 x_125) 1000)) (?v_155 (* (- x_32 x_119) 1000)) (?v_156 (* (- x_32 x_125) 1000)) (?v_159 (* (- x_35 x_119) 1000)) (?v_160 (* (- x_35 x_125) 1000)) (?v_163 (* (- x_38 x_119) 1000)) (?v_164 (* (- x_38 x_125) 1000)) (?v_167 (* (- x_18 x_119) 1000)) (?v_188 (- x_18 x_125))) (let ((?v_168 (* ?v_188 1000)) (?v_171 (- x_17 x_112)) (?v_173 (- x_26 x_120)) (?v_174 (- x_17 x_113)) (?v_176 (- x_29 x_121)) (?v_177 (- x_17 x_114)) (?v_179 (- x_32 x_122)) (?v_180 (- x_17 x_115)) (?v_182 (- x_35 x_123)) (?v_183 (- x_17 x_116)) (?v_185 (- x_38 x_124)) (?v_186 (- x_17 x_117)) (?v_189 (- x_17 x_118)) (?v_190 (- x_22 x_23)) (?v_192 (- x_25 x_26)) (?v_194 (- x_28 x_29)) (?v_195 (- x_31 x_32)) (?v_196 (- x_34 x_35)) (?v_197 (- x_37 x_38)) (?v_198 (- x_19 x_18)) (?v_207 (- x_1 x_1)) (?v_209 (- x_2 x_2)) (?v_211 (- x_3 x_3)) (?v_212 (- x_4 x_4)) (?v_213 (- x_5 x_5)) (?v_214 (- x_6 x_6)) (?v_215 (- x_7 x_7)) (?v_216 (- x_1 0)) (?v_217 (- 1 ?v_87)) (?v_221 (- x_2 0)) (?v_223 (- x_3 0)) (?v_224 (- x_4 0)) (?v_225 (- x_5 0)) (?v_226 (- x_6 0)) (?v_227 (- x_7 0)) (?v_235 (- ?v_87 1)) (?v_237 (- 0 x_2)) (?v_239 (- 0 x_3)) (?v_240 (- 0 x_4)) (?v_241 (- 0 x_5)) (?v_242 (- 0 x_6)) (?v_0 (+ x_0 (/ 999 1000))) (?v_1 (+ x_0 (/ 1001 1000))) (?v_191 (* (* x_9 999) (/ 1 1000))) (?v_193 (* (* x_9 1001) (/ 1 1000))) (?v_208 (* (* ?v_206 999) (/ 1 1000))) (?v_210 (* (* ?v_206 1001) (/ 1 1000)))) (let ((?v_220 (* (* ?v_217 999) (/ 1 1000))) (?v_222 (* (* ?v_217 1001) (/ 1 1000))) (?v_232 (and ?v_233 (or (not (>= (+ (+ (* (* (+ (+ (+ 1 (* ?v_230 (/ 1 999))) 1) (* ?v_231 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)) 0)) (> (- (- (* (* (+ (+ (+ 1 (* ?v_230 (/ 1 1001))) 1) (* ?v_231 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)) 0)))) (?v_236 (* (* ?v_235 999) (/ 1 1000))) (?v_238 (* (* ?v_235 1001) (/ 1 1000))) (?v_247 (and ?v_229 (or (not (<= ?v_191 ?v_246)) (not (<= ?v_246 ?v_193)))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_8 0)) (not (<= x_9 0))) (not (<= x_60 0))) (not (< x_126 (+ x_60 (* (* (+ (* (* x_9 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_127 (- (* (* (- (- x_9 x_126) 1) 999) (/ 1 2)) 1))) (not (< x_127 (* (* (+ (+ (+ x_8 x_60) x_126) (/ 1501 1000)) 1001) (/ 1 999))))) (not (<= x_128 0))) (<= x_128 (- x_8 (+ (+ x_60 (* (* (+ x_9 2) 1001) (/ 1 999))) (/ 1 2))))) (= x_0 0)) (<= ?v_0 x_1)) (<= x_1 ?v_1)) (<= ?v_0 x_2)) (<= x_2 ?v_1)) (<= ?v_0 x_3)) (<= x_3 ?v_1)) (<= ?v_0 x_4)) (<= x_4 ?v_1)) (<= ?v_0 x_5)) (<= x_5 ?v_1)) (<= ?v_0 x_6)) (<= x_6 ?v_1)) (<= ?v_0 x_7)) (<= x_7 ?v_1)) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (< x_0 x_1) (< x_0 x_2)) (< x_0 x_3)) (< x_0 x_4)) (< x_0 x_5)) (< x_0 x_6)) (< x_0 x_7)) (< x_0 x_61)) (<= x_61 x_1)) (<= x_61 x_2)) (<= x_61 x_3)) (<= x_61 x_4)) (<= x_61 x_5)) (<= x_61 x_6)) (<= x_61 x_7)) (or (or (or (or (or (or (= x_61 x_1) (= x_61 x_2)) (= x_61 x_3)) (= x_61 x_4)) (= x_61 x_5)) (= x_61 x_6)) (= x_61 x_7))) ?v_61) ?v_13) ?v_20) ?v_27) ?v_34) ?v_41) ?v_48) ?v_5) ?v_14) ?v_21) ?v_28) ?v_35) ?v_42) ?v_49) ?v_4) ?v_15) ?v_22) ?v_29) ?v_36) ?v_43) ?v_50) ?v_62) ?v_16) ?v_23) ?v_30) ?v_37) ?v_44) ?v_51) ?v_10) ?v_17) ?v_24) ?v_31) ?v_38) ?v_45) ?v_52) ?v_9) ?v_18) ?v_25) ?v_32) ?v_39) ?v_46) ?v_53) ?v_11) ?v_19) ?v_26) ?v_33) ?v_40) ?v_47) ?v_54) (= x_62 1)) (= x_63 1)) (= x_64 1)) (= x_65 1)) (= x_66 1)) (= x_67 1)) (= x_68 1)) (= x_69 1)) (= x_70 1)) (= x_71 1)) (= x_72 1)) (= x_73 1)) (= x_74 1)) (= x_75 1)) (= x_76 1)) (= x_77 1)) (= x_78 1)) (= x_79 1)) (= x_80 1)) (= x_81 1)) (= x_82 1)) (= x_83 1)) (= x_84 1)) (= x_85 1)) (= x_86 1)) (= x_87 1)) (= x_88 1)) (= x_89 1)) (= x_90 1)) (= x_91 1)) (= x_92 1)) (= x_93 1)) (= x_94 1)) (= x_95 1)) (= x_96 1)) (= x_97 1)) (= x_98 1)) (= x_99 1)) (= x_100 1)) (= x_101 1)) (= x_102 1)) (= x_103 1)) (= x_104 1)) (= x_105 1)) (= x_106 1)) (= x_107 1)) (= x_108 1)) (= x_109 1)) (= x_110 1)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_1) (<= ?v_0 x_53)) (<= x_53 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_2)) (<= ?v_2 ?v_57)) ?v_8) ?v_4) (and (and (and ?v_7 (= x_54 ?v_58)) (= x_10 ?v_59)) ?v_5)) (and (and (and ?v_12 ?v_8) ?v_5) ?v_4))) (or (or (and (and (and ?v_6 (= x_23 x_0)) ?v_9) ?v_10) (and (and (and ?v_7 (= x_22 x_0)) (= x_21 (- x_54 1))) ?v_11)) (and (and (and ?v_12 ?v_11) ?v_9) ?v_10))) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_2) (<= ?v_0 x_55)) (<= x_55 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_56)) (<= ?v_56 ?v_57)) ?v_60) ?v_15) (and (and (and ?v_7 (= x_46 ?v_58)) (= x_11 ?v_59)) ?v_14)) (and (and (and ?v_12 ?v_60) ?v_14) ?v_15))) (or (or (and (and (and ?v_6 (= x_26 x_0)) ?v_18) ?v_17) (and (and (and ?v_7 (= x_25 x_0)) (= x_24 (- x_46 1))) ?v_19)) (and (and (and ?v_12 ?v_19) ?v_18) ?v_17))) ?v_61) ?v_5) ?v_4) ?v_62) ?v_10) ?v_9) ?v_11) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_3) (<= ?v_0 x_56)) (<= x_56 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_63)) (<= ?v_63 ?v_57)) ?v_64) ?v_22) (and (and (and ?v_7 (= x_47 ?v_58)) (= x_12 ?v_59)) ?v_21)) (and (and (and ?v_12 ?v_64) ?v_21) ?v_22))) (or (or (and (and (and ?v_6 (= x_29 x_0)) ?v_25) ?v_24) (and (and (and ?v_7 (= x_28 x_0)) (= x_27 (- x_47 1))) ?v_26)) (and (and (and ?v_12 ?v_26) ?v_25) ?v_24))) ?v_61) ?v_5) ?v_4) ?v_62) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_4) (<= ?v_0 x_57)) (<= x_57 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_65)) (<= ?v_65 ?v_57)) ?v_66) ?v_29) (and (and (and ?v_7 (= x_48 ?v_58)) (= x_13 ?v_59)) ?v_28)) (and (and (and ?v_12 ?v_66) ?v_28) ?v_29))) (or (or (and (and (and ?v_6 (= x_32 x_0)) ?v_32) ?v_31) (and (and (and ?v_7 (= x_31 x_0)) (= x_30 (- x_48 1))) ?v_33)) (and (and (and ?v_12 ?v_33) ?v_32) ?v_31))) ?v_61) ?v_5) ?v_4) ?v_62) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_5) (<= ?v_0 x_58)) (<= x_58 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_67)) (<= ?v_67 ?v_57)) ?v_68) ?v_36) (and (and (and ?v_7 (= x_49 ?v_58)) (= x_14 ?v_59)) ?v_35)) (and (and (and ?v_12 ?v_68) ?v_35) ?v_36))) (or (or (and (and (and ?v_6 (= x_35 x_0)) ?v_39) ?v_38) (and (and (and ?v_7 (= x_34 x_0)) (= x_33 (- x_49 1))) ?v_40)) (and (and (and ?v_12 ?v_40) ?v_39) ?v_38))) ?v_61) ?v_5) ?v_4) ?v_62) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_6) (<= ?v_0 x_59)) (<= x_59 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_69)) (<= ?v_69 ?v_57)) ?v_70) ?v_43) (and (and (and ?v_7 (= x_50 ?v_58)) (= x_15 ?v_59)) ?v_42)) (and (and (and ?v_12 ?v_70) ?v_42) ?v_43))) (or (or (and (and (and ?v_6 (= x_38 x_0)) ?v_46) ?v_45) (and (and (and ?v_7 (= x_37 x_0)) (= x_36 (- x_50 1))) ?v_47)) (and (and (and ?v_12 ?v_47) ?v_46) ?v_45))) ?v_61) ?v_5) ?v_4) ?v_62) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_48) ?v_49) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_7) (<= ?v_0 x_51)) (<= x_51 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_55 ?v_71)) (<= ?v_71 ?v_57)) ?v_72) ?v_50) (and (and (and ?v_7 (= x_52 ?v_58)) (= x_16 ?v_59)) ?v_49)) (and (and (and ?v_12 ?v_72) ?v_49) ?v_50))) (or (or (and (and (and ?v_6 (= x_18 x_0)) ?v_53) ?v_52) (and (and (and ?v_7 (= x_19 x_0)) (= x_20 (- x_52 1))) ?v_54)) (and (and (and ?v_12 ?v_54) ?v_53) ?v_52))) ?v_61) ?v_5) ?v_4) ?v_62) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47)) (<= ?v_73 x_62)) (<= ?v_73 x_69)) (<= ?v_73 x_76)) (<= ?v_73 x_83)) (<= ?v_73 x_90)) (<= ?v_73 x_97)) (<= ?v_73 x_104)) (<= ?v_74 x_63)) (<= ?v_74 x_70)) (<= ?v_74 x_77)) (<= ?v_74 x_84)) (<= ?v_74 x_91)) (<= ?v_74 x_98)) (<= ?v_74 x_105)) (<= ?v_75 x_64)) (<= ?v_75 x_71)) (<= ?v_75 x_78)) (<= ?v_75 x_85)) (<= ?v_75 x_92)) (<= ?v_75 x_99)) (<= ?v_75 x_106)) (<= ?v_76 x_65)) (<= ?v_76 x_72)) (<= ?v_76 x_79)) (<= ?v_76 x_86)) (<= ?v_76 x_93)) (<= ?v_76 x_100)) (<= ?v_76 x_107)) (<= ?v_77 x_66)) (<= ?v_77 x_73)) (<= ?v_77 x_80)) (<= ?v_77 x_87)) (<= ?v_77 x_94)) (<= ?v_77 x_101)) (<= ?v_77 x_108)) (<= ?v_78 x_67)) (<= ?v_78 x_74)) (<= ?v_78 x_81)) (<= ?v_78 x_88)) (<= ?v_78 x_95)) (<= ?v_78 x_102)) (<= ?v_78 x_109)) (<= ?v_79 x_68)) (<= ?v_79 x_75)) (<= ?v_79 x_82)) (<= ?v_79 x_89)) (<= ?v_79 x_96)) (<= ?v_79 x_103)) (<= ?v_79 x_110)) (<= x_62 ?v_80)) (<= x_69 ?v_80)) (<= x_76 ?v_80)) (<= x_83 ?v_80)) (<= x_90 ?v_80)) (<= x_97 ?v_80)) (<= x_104 ?v_80)) (<= x_63 ?v_81)) (<= x_70 ?v_81)) (<= x_77 ?v_81)) (<= x_84 ?v_81)) (<= x_91 ?v_81)) (<= x_98 ?v_81)) (<= x_105 ?v_81)) (<= x_64 ?v_82)) (<= x_71 ?v_82)) (<= x_78 ?v_82)) (<= x_85 ?v_82)) (<= x_92 ?v_82)) (<= x_99 ?v_82)) (<= x_106 ?v_82)) (<= x_65 ?v_83)) (<= x_72 ?v_83)) (<= x_79 ?v_83)) (<= x_86 ?v_83)) (<= x_93 ?v_83)) (<= x_100 ?v_83)) (<= x_107 ?v_83)) (<= x_66 ?v_84)) (<= x_73 ?v_84)) (<= x_80 ?v_84)) (<= x_87 ?v_84)) (<= x_94 ?v_84)) (<= x_101 ?v_84)) (<= x_108 ?v_84)) (<= x_67 ?v_85)) (<= x_74 ?v_85)) (<= x_81 ?v_85)) (<= x_88 ?v_85)) (<= x_95 ?v_85)) (<= x_102 ?v_85)) (<= x_109 ?v_85)) (<= x_68 ?v_86)) (<= x_75 ?v_86)) (<= x_82 ?v_86)) (<= x_89 ?v_86)) (<= x_96 ?v_86)) (<= x_103 ?v_86)) (<= x_110 ?v_86)) (= x_61 x_0)))) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not ?v_88) (not ?v_89)) (not ?v_90)) (not ?v_91)) (not ?v_92)) (not ?v_93)) (not ?v_94)) (= x_111 x_61)) (= x_112 x_54)) (= x_113 x_46)) (= x_114 x_47)) (= x_115 x_48)) (= x_116 x_49)) (= x_117 x_50)) (= x_118 x_52)) (= x_119 x_53)) (= x_120 x_55)) (= x_121 x_56)) (= x_122 x_57)) (= x_123 x_58)) (= x_124 x_59)) (= x_125 x_51)) (= x_17 ?v_202)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or ?v_88 ?v_89) ?v_90) ?v_91) ?v_92) ?v_93) ?v_94) (= x_17 ?v_87)) (= x_111 x_0)) (= x_119 x_1)) (= x_120 x_2)) (= x_121 x_3)) (= x_122 x_4)) (= x_123 x_5)) (= x_124 x_6)) (= x_125 x_7)) (= x_112 1)) (= x_113 1)) (= x_114 1)) (= x_115 1)) (= x_116 1)) (= x_117 1)) (= x_118 1)))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (not (<= ?v_95 x_112)) (not (<= ?v_95 x_113))) (not (<= ?v_95 x_114))) (not (<= ?v_95 x_115))) (not (<= ?v_95 x_116))) (not (<= ?v_95 x_117))) (not (<= ?v_95 x_118))) (not (<= x_112 ?v_96))) (not (<= x_113 ?v_96))) (not (<= x_114 ?v_96))) (not (<= x_115 ?v_96))) (not (<= x_116 ?v_96))) (not (<= x_117 ?v_96))) (not (<= x_118 ?v_96))) (not (<= (- x_112 x_112) x_126))) (not (<= (- x_113 x_112) x_126))) (not (<= (- x_114 x_112) x_126))) (not (<= (- x_115 x_112) x_126))) (not (<= (- x_116 x_112) x_126))) (not (<= (- x_117 x_112) x_126))) (not (<= (- x_118 x_112) x_126))) (not (<= (- x_112 x_113) x_126))) (not (<= (- x_113 x_113) x_126))) (not (<= (- x_114 x_113) x_126))) (not (<= (- x_115 x_113) x_126))) (not (<= (- x_116 x_113) x_126))) (not (<= (- x_117 x_113) x_126))) (not (<= (- x_118 x_113) x_126))) (not (<= (- x_112 x_114) x_126))) (not (<= (- x_113 x_114) x_126))) (not (<= (- x_114 x_114) x_126))) (not (<= (- x_115 x_114) x_126))) (not (<= (- x_116 x_114) x_126))) (not (<= (- x_117 x_114) x_126))) (not (<= (- x_118 x_114) x_126))) (not (<= (- x_112 x_115) x_126))) (not (<= (- x_113 x_115) x_126))) (not (<= (- x_114 x_115) x_126))) (not (<= (- x_115 x_115) x_126))) (not (<= (- x_116 x_115) x_126))) (not (<= (- x_117 x_115) x_126))) (not (<= (- x_118 x_115) x_126))) (not (<= (- x_112 x_116) x_126))) (not (<= (- x_113 x_116) x_126))) (not (<= (- x_114 x_116) x_126))) (not (<= (- x_115 x_116) x_126))) (not (<= (- x_116 x_116) x_126))) (not (<= (- x_117 x_116) x_126))) (not (<= (- x_118 x_116) x_126))) (not (<= (- x_112 x_117) x_126))) (not (<= (- x_113 x_117) x_126))) (not (<= (- x_114 x_117) x_126))) (not (<= (- x_115 x_117) x_126))) (not (<= (- x_116 x_117) x_126))) (not (<= (- x_117 x_117) x_126))) (not (<= (- x_118 x_117) x_126))) (not (<= (- x_112 x_118) x_126))) (not (<= (- x_113 x_118) x_126))) (not (<= (- x_114 x_118) x_126))) (not (<= (- x_115 x_118) x_126))) (not (<= (- x_116 x_118) x_126))) (not (<= (- x_117 x_118) x_126))) (not (<= (- x_118 x_118) x_126))) (and (or ?v_99 (not (<= x_54 ?v_97))) (not ?v_142))) (and (or ?v_100 (not (<= x_46 ?v_97))) (not ?v_146))) (and (or ?v_101 (not (<= x_47 ?v_97))) (not ?v_150))) (and (or ?v_102 (not (<= x_48 ?v_97))) (not ?v_154))) (and (or ?v_103 (not (<= x_49 ?v_97))) (not ?v_158))) (and (or ?v_104 (not (<= x_50 ?v_97))) (not ?v_162))) (and (or ?v_105 (not (<= x_52 ?v_97))) (not ?v_166))) (and (and (and (and (and (and ?v_99 ?v_100) ?v_101) ?v_102) ?v_103) ?v_104) ?v_105)) (and ?v_106 (or (not (<= (* (* ?v_108 999) (/ 1 1000)) ?v_107)) (not (<= ?v_107 (* (* ?v_108 1001) (/ 1 1000))))))) (and ?v_109 (or (not (<= (* (* ?v_111 999) (/ 1 1000)) ?v_110)) (not (<= ?v_110 (* (* ?v_111 1001) (/ 1 1000))))))) (and ?v_112 (or (not (<= (* (* ?v_114 999) (/ 1 1000)) ?v_113)) (not (<= ?v_113 (* (* ?v_114 1001) (/ 1 1000))))))) (and ?v_115 (or (not (<= (* (* ?v_117 999) (/ 1 1000)) ?v_116)) (not (<= ?v_116 (* (* ?v_117 1001) (/ 1 1000))))))) (and ?v_118 (or (not (<= (* (* ?v_120 999) (/ 1 1000)) ?v_119)) (not (<= ?v_119 (* (* ?v_120 1001) (/ 1 1000))))))) (and ?v_121 (or (not (<= (* (* ?v_123 999) (/ 1 1000)) ?v_122)) (not (<= ?v_122 (* (* ?v_123 1001) (/ 1 1000))))))) (and ?v_124 (or (not (<= (* (* ?v_126 999) (/ 1 1000)) ?v_125)) (not (<= ?v_125 (* (* ?v_126 1001) (/ 1 1000))))))) (and (and ?v_106 ?v_141) (or (or (< x_61 x_23) (not (<= (* (* ?v_128 999) (/ 1 1000)) ?v_127))) (not (<= ?v_127 (* (* ?v_128 1001) (/ 1 1000))))))) (and (and ?v_109 ?v_145) (or (or (< x_61 x_26) (not (<= (* (* ?v_130 999) (/ 1 1000)) ?v_129))) (not (<= ?v_129 (* (* ?v_130 1001) (/ 1 1000))))))) (and (and ?v_112 ?v_149) (or (or (< x_61 x_29) (not (<= (* (* ?v_132 999) (/ 1 1000)) ?v_131))) (not (<= ?v_131 (* (* ?v_132 1001) (/ 1 1000))))))) (and (and ?v_115 ?v_153) (or (or (< x_61 x_32) (not (<= (* (* ?v_134 999) (/ 1 1000)) ?v_133))) (not (<= ?v_133 (* (* ?v_134 1001) (/ 1 1000))))))) (and (and ?v_118 ?v_157) (or (or (< x_61 x_35) (not (<= (* (* ?v_136 999) (/ 1 1000)) ?v_135))) (not (<= ?v_135 (* (* ?v_136 1001) (/ 1 1000))))))) (and (and ?v_121 ?v_161) (or (or (< x_61 x_38) (not (<= (* (* ?v_138 999) (/ 1 1000)) ?v_137))) (not (<= ?v_137 (* (* ?v_138 1001) (/ 1 1000))))))) (and (and ?v_124 ?v_165) (or (or (< x_61 x_18) (not (<= (* (* ?v_140 999) (/ 1 1000)) ?v_139))) (not (<= ?v_139 (* (* ?v_140 1001) (/ 1 1000))))))) (and ?v_169 (or (not (<= x_39 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_143 (/ 1 999))) x_118) (* ?v_144 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_39 (- (- (* (* (+ (+ (+ x_112 (* ?v_143 (/ 1 1001))) x_118) (* ?v_144 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_172 (or (not (<= x_40 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_147 (/ 1 999))) x_118) (* ?v_148 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_40 (- (- (* (* (+ (+ (+ x_112 (* ?v_147 (/ 1 1001))) x_118) (* ?v_148 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_175 (or (not (<= x_41 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_151 (/ 1 999))) x_118) (* ?v_152 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_41 (- (- (* (* (+ (+ (+ x_112 (* ?v_151 (/ 1 1001))) x_118) (* ?v_152 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_178 (or (not (<= x_42 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_155 (/ 1 999))) x_118) (* ?v_156 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_42 (- (- (* (* (+ (+ (+ x_112 (* ?v_155 (/ 1 1001))) x_118) (* ?v_156 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_181 (or (not (<= x_43 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_159 (/ 1 999))) x_118) (* ?v_160 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_43 (- (- (* (* (+ (+ (+ x_112 (* ?v_159 (/ 1 1001))) x_118) (* ?v_160 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_184 (or (not (<= x_44 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_163 (/ 1 999))) x_118) (* ?v_164 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_44 (- (- (* (* (+ (+ (+ x_112 (* ?v_163 (/ 1 1001))) x_118) (* ?v_164 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_187 (or (not (<= x_45 (+ (+ (* (* (+ (+ (+ x_112 (* ?v_167 (/ 1 999))) x_118) (* ?v_168 (/ 1 999))) 1) (/ 1 2)) x_60) (/ 3001 1998)))) (< x_45 (- (- (* (* (+ (+ (+ x_112 (* ?v_167 (/ 1 1001))) x_118) (* ?v_168 (/ 1 1001))) 1) (/ 1 2)) x_60) (/ 1 2)))))) (and ?v_169 (or (not (<= (* (* ?v_171 999) (/ 1 1000)) ?v_170)) (not (<= ?v_170 (* (* ?v_171 1001) (/ 1 1000))))))) (and ?v_172 (or (not (<= (* (* ?v_174 999) (/ 1 1000)) ?v_173)) (not (<= ?v_173 (* (* ?v_174 1001) (/ 1 1000))))))) (and ?v_175 (or (not (<= (* (* ?v_177 999) (/ 1 1000)) ?v_176)) (not (<= ?v_176 (* (* ?v_177 1001) (/ 1 1000))))))) (and ?v_178 (or (not (<= (* (* ?v_180 999) (/ 1 1000)) ?v_179)) (not (<= ?v_179 (* (* ?v_180 1001) (/ 1 1000))))))) (and ?v_181 (or (not (<= (* (* ?v_183 999) (/ 1 1000)) ?v_182)) (not (<= ?v_182 (* (* ?v_183 1001) (/ 1 1000))))))) (and ?v_184 (or (not (<= (* (* ?v_186 999) (/ 1 1000)) ?v_185)) (not (<= ?v_185 (* (* ?v_186 1001) (/ 1 1000))))))) (and ?v_187 (or (not (<= (* (* ?v_189 999) (/ 1 1000)) ?v_188)) (not (<= ?v_188 (* (* ?v_189 1001) (/ 1 1000))))))) (and ?v_142 (not (= x_21 (+ x_39 x_9))))) (and ?v_146 (not (= x_24 (+ x_40 x_9))))) (and ?v_150 (not (= x_27 (+ x_41 x_9))))) (and ?v_154 (not (= x_30 (+ x_42 x_9))))) (and ?v_158 (not (= x_33 (+ x_43 x_9))))) (and ?v_162 (not (= x_36 (+ x_44 x_9))))) (and ?v_166 (not (= x_20 (+ x_45 x_9))))) (and ?v_142 (or (not (<= ?v_191 ?v_190)) (not (<= ?v_190 ?v_193))))) (and ?v_146 (or (not (<= ?v_191 ?v_192)) (not (<= ?v_192 ?v_193))))) (and ?v_150 (or (not (<= ?v_191 ?v_194)) (not (<= ?v_194 ?v_193))))) (and ?v_154 (or (not (<= ?v_191 ?v_195)) (not (<= ?v_195 ?v_193))))) (and ?v_158 (or (not (<= ?v_191 ?v_196)) (not (<= ?v_196 ?v_193))))) (and ?v_162 (or (not (<= ?v_191 ?v_197)) (not (<= ?v_197 ?v_193))))) (and ?v_166 (or (not (<= ?v_191 ?v_198)) (not (<= ?v_198 ?v_193))))) ?v_199) ?v_199) ?v_199) ?v_199) ?v_199) ?v_199) ?v_199) ?v_200) ?v_200) ?v_200) ?v_200) ?v_200) ?v_200) ?v_200) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_201) ?v_203) ?v_203) ?v_203) ?v_203) ?v_203) ?v_203) ?v_203) (and (and (and (and (and (and ?v_204 ?v_204) ?v_204) ?v_204) ?v_204) ?v_204) ?v_204)) (and ?v_205 (or (not (<= ?v_208 ?v_207)) (not (<= ?v_207 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_209)) (not (<= ?v_209 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_211)) (not (<= ?v_211 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_212)) (not (<= ?v_212 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_213)) (not (<= ?v_213 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_214)) (not (<= ?v_214 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_215)) (not (<= ?v_215 ?v_210))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_216))) (not (<= ?v_216 ?v_222))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_221))) (not (<= ?v_221 ?v_222))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_223))) (not (<= ?v_223 ?v_222))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_224))) (not (<= ?v_224 ?v_222))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_225))) (not (<= ?v_225 ?v_222))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_226))) (not (<= ?v_226 ?v_222))))) (and ?v_218 (or (or ?v_219 (not (<= ?v_220 ?v_227))) (not (<= ?v_227 ?v_222))))) ?v_232) ?v_232) ?v_232) ?v_232) ?v_232) ?v_232) ?v_232) (and ?v_233 (or (not (<= ?v_236 ?v_234)) (not (<= ?v_234 ?v_238))))) (and ?v_233 (or (not (<= ?v_236 ?v_237)) (not (<= ?v_237 ?v_238))))) (and ?v_233 (or (not (<= ?v_236 ?v_239)) (not (<= ?v_239 ?v_238))))) (and ?v_233 (or (not (<= ?v_236 ?v_240)) (not (<= ?v_240 ?v_238))))) (and ?v_233 (or (not (<= ?v_236 ?v_241)) (not (<= ?v_241 ?v_238))))) (and ?v_233 (or (not (<= ?v_236 ?v_242)) (not (<= ?v_242 ?v_238))))) (and ?v_233 (or (not (<= ?v_236 ?v_243)) (not (<= ?v_243 ?v_238))))) ?v_245) ?v_245) ?v_245) ?v_245) ?v_245) ?v_245) ?v_245) ?v_247) ?v_247) ?v_247) ?v_247) ?v_247) ?v_247) ?v_247)))))))))))))))))))))))))))
(check-sat)
(exit)
